Nuprl Lemma : finite_wf
4,23
postcript
pdf
T
:Type. finite(
T
)
Prop
latex
Definitions
finite(
T
)
,
P
Q
,
Prop
,
Inj(
A
;
B
;
f
)
,
Surj(
A
;
B
;
f
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
surject
wf
,
inject
wf
origin
T:Type. finite(T) 
Prop T:Type. finite(T) Prop 
Qx:A. B(x) T